hybrid 論理
hybrid logic
satisfaction 演算子$ @
$ @_i pis true iff$ pis true in the unique state named by the nominal$ i(i.e., the state where$ iis true)
Kripke model$ (W,R,\Vdash)に於いて、場所$ w\in Wでのみ眞になる命題$ i(nominal)$ w\Vdash iが在れば、場所$ wでのみ眞である命題$ @_i p(satisfaction statement) を表現できる。nominal に就いての satisfaction 演算子$ @_iで場所$ wを他の場所から區別できる 等價性が成り立つ
推移律$ @_a b\land @_b c\to @_a c Leibniz' law$ (a=b\land\phi(a))\to\phi(b)は$ @_a b\land @_a\phi\to @_b\phiと表現される
binder$ \forall、$ \downarrow
$ \forall a\phiThe$ \forallbinder quantifies over points analogous to the standard first-order universal quantifier, that is,$ \forall a\phiis true relative to$ wiff whatever point the nominal$ arefers to, it is the case that$ \phiis true relative to$ w
Kripke model$ (W,R,\Vdash)に於いて$ \forall a\phiが眞であるとは、nominal$ aの指す場所$ w\Vdash aと關係する全ての場所$ \forall v_{\in W}wRvで式$ \phiが眞である事を言ふ $ \downarrow a\phiThe$ \downarrowbinder binds$ anominal to the point of evaluation, that is,$ \downarrow a\phiis true relative to$ wiff$ \phiis true relative to$ wwhen$ arefers to$ w
Kripke model$ (W,R,\Vdash)に於いて$ \downarrow a\phiが眞であるとは、場所$ w,vを$ w\Vdash a且つ$ v\Vdash a且つ$ wRvである場所として、場所$ vに於いて式$ \phiが眞である事を言ふ $ \downarrow a\phi\iff\forall a(a\to\phi).